a:, b:. ((-a) rem b) = (-(a rem b)) 

latex

Up	int 2, int 2
Definitions	t  T, x:A. B(x), P  Q, P & Q, P  Q, P  Q, False, {...i}, A  B, A, , P  Q, Dec(P), , , a  b  T
Lemmas	int nzero wf, nat plus wf, decidable le, rem 2 to 1, le wf, minus functionality wrt eq, rem sym